PRISM
=====
Version: 4.5.dev
Date: Fri Feb 26 16:41:53 CET 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 ij.30.prism ij.30.props --property stable
Parsing model file "ij.30.prism"...
Type: MDP
Modules: process0 process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29
Variables: q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 q13 q14 q15 q16 q17 q18 q19 q20 q21 q22 q23 q24 q25 q26 q27 q28 q29 num_tokens_var
Parsing properties file "ij.30.props"...
1 property:
(1) "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29)=1) ]
---------------------------------------------------------------------
Model checking: "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29)=1) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 30 iterations in 0.01 seconds (average 0.000267, setup 0.00)
Time for model construction: 0.035 seconds.
Type: MDP
States: 1073741823 (1 initial)
Transitions: 28185722880
Choices: 16106127360
Transition matrix: 2429 nodes (3 terminal), 28185722880 minterms, vars: 35r/35c/29nd
Warning: Switching to MTBDD engine (default for heuristic=speed and this state space size).
Prob0A: 30 iterations in 0.20 seconds (average 0.006700, setup 0.00)
Prob1E: 31 iterations in 0.27 seconds (average 0.008677, setup 0.00)
yes = 1073741823, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 0.475 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 0.752 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.